\begin{tabbing}
plus{-}ify\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it ff}$; ${\it is\_req}$; ${\it is\_ack}$; ${\it awaiting}$; ${\it owes\_ack}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:${\it ff}$.C, $j$:${\it ff}$.C.\+
\\[0ex]es{-}initially(${\it es}$;$i$;${\it owes\_ack}$($i$,$j$)) = ff $\in$ $\mathbb{B}$ \& es{-}initially(${\it es}$;$i$;${\it awaiting}$($i$,$j$)) = ff $\in$ $\mathbb{B}$
\\[0ex]\& (\=$\forall$$e$:es{-}E(${\it es}$).\+
\\[0ex](snd{-}it(${\it ff}$;${\it is\_req}$;$e$;$i$;$j$) $\Rightarrow$ (es{-}when(${\it es}$; (${\it awaiting}$($i$,$j$)); $e$) = ff $\in$ $\mathbb{B}$))
\\[0ex]\& (rcv{-}it(${\it ff}$;${\it is\_ack}$;$e$;$i$;$j$) $\Rightarrow$ (es{-}after(${\it es}$; (${\it awaiting}$($i$,$j$)); $e$) = ff $\in$ $\mathbb{B}$))
\\[0ex]\& (snd{-}it(${\it ff}$;${\it is\_req}$;$e$;$i$;$j$) $\Rightarrow$ (es{-}after(${\it es}$; (${\it awaiting}$($i$,$j$)); $e$) = tt $\in$ $\mathbb{B}$))
\\[0ex]\& (\=(es{-}loc(${\it es}$; $e$) = $i$ $\in$ Id\+
\\[0ex]\& ($\neg$(es{-}after(${\it es}$; (${\it awaiting}$($i$,$j$)); $e$) = es{-}when(${\it es}$; (${\it awaiting}$($i$,$j$)); $e$) $\in$ $\mathbb{B}$)))
\\[0ex]$\Rightarrow$ (rcv{-}it(${\it ff}$;${\it is\_ack}$;$e$;$i$;$j$) $\vee$ snd{-}it(${\it ff}$;${\it is\_req}$;$e$;$i$;$j$)))
\-\\[0ex]\& (snd{-}it(${\it ff}$;${\it is\_ack}$;$e$;$i$;$j$) $\Rightarrow$ (es{-}when(${\it es}$; (${\it owes\_ack}$($i$,$j$)); $e$) = tt $\in$ $\mathbb{B}$))
\\[0ex]\& (rcv{-}it(${\it ff}$;${\it is\_req}$;$e$;$i$;$j$) $\Rightarrow$ (es{-}after(${\it es}$; (${\it owes\_ack}$($i$,$j$)); $e$) = tt $\in$ $\mathbb{B}$))
\\[0ex]\& (snd{-}it(${\it ff}$;${\it is\_ack}$;$e$;$i$;$j$) $\Rightarrow$ (es{-}after(${\it es}$; (${\it owes\_ack}$($i$,$j$)); $e$) = ff $\in$ $\mathbb{B}$))
\\[0ex]\& (\=(es{-}loc(${\it es}$; $e$) = $i$ $\in$ Id\+
\\[0ex]\& ($\neg$(es{-}after(${\it es}$; (${\it owes\_ack}$($i$,$j$)); $e$) = es{-}when(${\it es}$; (${\it owes\_ack}$($i$,$j$)); $e$) $\in$ $\mathbb{B}$)))
\\[0ex]$\Rightarrow$ (rcv{-}it(${\it ff}$;${\it is\_req}$;$e$;$i$;$j$) $\vee$ snd{-}it(${\it ff}$;${\it is\_ack}$;$e$;$i$;$j$)))
\-\\[0ex]\& (\=((es{-}loc(${\it es}$; $e$) = $i$ $\in$ Id) c$\wedge$ (es{-}after(${\it es}$; (${\it owes\_ack}$($i$,$j$)); $e$) = tt $\in$ $\mathbb{B}$))\+
\\[0ex]$\Rightarrow$ ($\exists$${\it e'}$:es{-}E(${\it es}$). (es{-}causl(${\it es}$; $e$; ${\it e'}$) \& snd{-}it(${\it ff}$;${\it is\_ack}$;${\it e'}$;$i$;$j$)))))
\-\-\-
\end{tabbing}